;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "iBlur.lisp")
(require "mBlur.lisp")
;(require "mImage.lisp")
;(require "mCommon.lisp")

(module tBlur
  (import iBlur)
  ;(import iImage)
  (include-book "testing" :dir :teachpacks)
  (include-book "doublecheck" :dir :teachpacks)
  (include-book "avl-rational-keys" :dir :teachpacks)
  
;  (defun include_meta_data (tr)
;    (avl-insert (avl-insert (avl-insert tr -1 ()) -2 ()) -3 ())) 
;     
;  (check-expect (include_meta_data ()) (flip-v (include_meta_data ())))
;  (check-expect (include_meta_data ()) (flip-h (include_meta_data ())))
;  
;  (defrandom bld_tr (tr w h w_org)
;    (if (equal w 0)
;        (if (equal h 0)              
;            (insertPixel tr w h (random-between 0 255) (random-between 0 255) (random-between 0 255))
;            (bld_tr (insertPixel tr w h (random-between 0 255) (random-between 0 255) (random-between 0 255)) w_org (1- h) w_org))
;        (bld_tr (insertPixel tr w h (random-between 0 255) (random-between 0 255) (random-between 0 255)) (1- w) h w_org)))
;  
;  (defproperty p1 :repeat 100
;    (width  :value (random-between 1 64)
;            height :value (random-between 1 64)
;            img    :value (bld_tr () width height width))
;    (equal (flip-v (flip-v (include_meta_data img))) (include_meta_data img)))
;  
;    (defproperty p2 :repeat 100
;    (width  :value (random-between 1 64)
;            height :value (random-between 1 64)
;            img    :value (bld_tr () width height width))
;    (equal (flip-h (flip-h (include_meta_data img))) (include_meta_data img)))
;  
;  (check-properties)
  )

(link tstBlur (;mCommon mImage 
               mBlur tBlur))

(invoke tstBlur)